package river_city_ransom.services;

import exceptions.ComposantError;


public interface Personnage extends Equipable {
	/** _________________________________________________________ OBSERVATORS */
	public String nom();
	public int force();
	public int maxPointsDeVie();
	public int pointsDeVie();
	public boolean estVaincu();
	public Equipable choseEquipee();
	public boolean estEquipe();
	public int estGele();
	public boolean versLaDroite();
	
	
	/** __________________________________________________________ INVARIANTS */
//	inv estEquipable(P) = estGele(P) > 0
//	inv (estPorte(P) v estJete(P) != 0) -> estGele(P) > 0
//	inv pointsDeVie(P) <= maxPointsDeVie(P)
//	inv estVaincu(P) = pointsDeVie(P) <= 0
//	inv estEquipe(P) = choseEquipee(P) != NULL
//	inv estGele(P) >= 0
	
	
	/** ___________________________________________________________ OPERATORS */
//	pre deposerPointsDeVie(P, pv) require estGele(P) = 0 ^ pv > 0
//	post pointsDeVie(deposerPointsDeVie(P, pv)) = min(pointsDeVie(P) + pv, maxPointsDeVie(P))
//	post estPorte(deposerPointsDeVie(P, pv)) = estPorte(P)
//	post estJete(deposerPointsDeVie(P, pv)) = estJete(P)
//	post choseEquipee(deposerPointsDeVie(P, pv)) = choseEquipee(P)
//	post position(deposerPointsDeVie(P, pv)) = position(P)
//	post versLaDroite(deposerPointsDeVie(P, pv)) = versLaDroite(P)
//	post estGele(deposerPointsDeVie(P, pv)) = estGele(P)
	public void deposerPointsDeVie(int pv) throws ComposantError;
	
//	pre retirerPointsDeVie(P, pv) require !estVaincu(P) ^ pv > 0
//	post pointsDeVie(retirerPointsDeVie(P, pv)) = max(0, pointsDeVie(P) - pv)
//	post estPorte(retirerPointsDeVie(P, pv)) = estPorte(P)
//	post estJete(retirerPointsDeVie(P, pv)) = estJete(P)
//	post choseEquipee(retirerPointsDeVie(P, pv)) = choseEquipee(P)
//	post position(retirerPointsDeVie(P, pv)) = position(P)
//	post versLaDroite(retirerPointsDeVie(P, pv)) = versLaDroite(P)
//	post estGele(retirerPointsDeVie(P, pv)) = estGele(P)
	public void retirerPointsDeVie(int pv) throws ComposantError;
	
//	pre ramasser(P, E) require !estVaincu(P) ^ estGele(P) = 0 ^ !estEquipe(P) ^ estEquipable(E) ^ !estPorte(E)
//	post choseEquipee(ramasser(P, E)) = O
//	post estPorte(ramasser(P, E)) = estPorte(P)
//	post estJete(ramasser(P, E)) = estJete(P)
//	post pointsDeVie(ramasser(P, E)) = pointsDeVie(P)
//	post position(ramasser(P, E)) = position(P)
//	post versLaDroite(ramasser(P, E)) = versLaDroite(P)
//	post estGele(ramasser(P, E)) = estGele(P)
	public void ramasser(Equipable e) throws ComposantError;
	
//	pre jeter(P) require !estVaincu(P) ^ estGele(P) = 0 ^ estEquipe(P)
//	post choseEquipee(jeter(P)) = NULL
//	post pointsDeVie(jeter(P)) = pointsDeVie(P)
//	post estPorte(jeter(P)) = estPorte(P)
//	post estJete(jeter(P)) = estJete(P)
//	post position(jeter(P)) = position(P)
//	post versLaDroite(jeter(P)) = versLaDroite(P)
//	post estGele(jeter(P)) = estGele(P)
	public void jeter() throws ComposantError;
	
//	pre deplacer(P, p) require !estVaincu(P) ^ estGele(P) = 0
//	post position(deplacer(P, p)) = p
//	post versLaDroite(deplacer(P, p)) = { true si Position::x(p) > Position::x(position(P))
//										{ false si Position::x(p) < Position::x(position(P))
//										{ versLaDroite(P) sinon
//	post pointsDeVie(deplacer(P, p)) = pointsDeVie(P)
//	post estPorte(deplacer(P, p)) = estPorte(P)
//	post estJete(deplacer(P, p)) = estJete(P)
//	post choseEquipee(deplacer(P, p)) = choseEquipee(P)
//	post estGele(deplacer(P, p)) = estGele(P)
	public void deplacer(Position p) throws ComposantError;
	
//	pre geler(P, g) require !estVaincu(P) ^ g > 0
//	post estGele(geler(P, g)) = g
//	post pointsDeVie(geler(P, g)) = pointsDeVie(P)
//	post estPorte(geler(P, g)) = estPorte(P)
//	post estJete(geler(P, g)) = estJete(P)
//	post choseEquipee(geler(P, g)) = choseEquipee(P)
//	post position(geler(P, g)) = position(P)
//	post versLaDroite(geler(P, g)) = versLaDroite(P)
	public void geler(int g) throws ComposantError;
	
//	post estGele(degeler(P)) = { max(0, estGele(P) - 1) si !estPorte(P)
//							   { estGele(P) sinon
//	post pointsDeVie(degeler(P)) = pointsDeVie(P)
//	post estPorte(degeler(P)) = estPorte(P)
//	post estJete(degeler(P)) = estJete(P)
//	post choseEquipee(degeler(P)) = choseEquipee(P)
//	post position(degeler(P)) = position(P)
//	post versLaDroite(degeler(P)) = versLaDroite(P)
	public void degeler() throws ComposantError;
}
